As usage of electronic devices increases, so does the number of software programs run on these devices. Typically when a software program is developed, it is verified to help assure that the software program satisfies all of the predetermined requirements for the software program. Developing test cases to determine if a software program satisfies all predetermined requirements may be difficult and time consuming.
A software application may include any number of programs (e.g., classes, functions, procedures, subroutines, modules, or code blocks), and each program may be tested or validated individually. A program may be tested or validated manually or automatically. In the former case, a person (e.g., a software testing engineer) may manually design test cases for the program based on the design specification of the program, execute the program under the test cases, and check for program behavior or output that does not agree with the test cases. In the later case, a software-testing tool, implemented as computer software or hardware, may generate test cases for a program under test, execute the program under test while simulating the test cases, and check for program behavior or output that does not agree with the test cases. The sheer complexity of modern software often renders manual generation or design of test cases inadequate for completely testing the program.
A program may be formally tested and validated by assigning test input values to input variables of the program and the output values resulting from the input variables may be analyzed to determine the behavior and validate the program. Symbolic execution may be used to automatically generate test input values to be used for testing the program. For example, a software-testing tool may use symbolic execution to determine which inputs cause each part of the program to execute by utilizing symbolic values in place of concrete values to create symbolic expressions and constraints to identify possible outcomes for each conditional branch in the program.
Symbolic execution refers to the analysis of programs by tracking symbolic rather than actual values, as a case of abstract interpretation. It is a non-explicit state model checking technique that treats input to programs as symbol variables. It creates complex equations by executing finite paths in the program with symbolic variables and then solves the complex equations with a solver to obtain error scenarios, if any. In contrast to explicit state model checking, symbolic execution may, in some embodiments, be able to work out all possible input values and all possible use cases of all possible input values in the program under analysis. Thus, symbolic execution may exhaustively validate a program under analysis.
The subject matter claimed herein is not limited to embodiments that solve any disadvantages or that operate only in environments such as those described above. Rather, this background is only provided to illustrate one example technology area where some embodiments described herein may be practiced.